\begin{tabbing}
$\forall$\=${\it poss}$:(ES\{i\}$\rightarrow\mathbb{P}$\{i'\}), $T$:Type\{i\}, $s$:$T$, $i$:Id, $P$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow\mathbb{P}$\{i'\}),\+
\\[0ex]$R$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$possible{-}event\{i:l\}(${\it poss}$)$\rightarrow\mathbb{P}$\{i'\}), ${\it Rs}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$\{i'\}).
\-\\[0ex]Trans(possible{-}event\=\{i:l\}\+
\\[0ex](${\it poss}$);$1$,$2$.$R$($1$,$2$))
\-\\[0ex]$\Rightarrow$ ma{-}knows\=\{i:l\}\+
\\[0ex](${\it poss}$; $i$; $T$; $s$; $P$; ${\it Rs}$; $R$)
\-\\[0ex]$\Rightarrow$ ma{-}knows\=\{i:l\}\+
\\[0ex](${\it poss}$; $i$; $T$; $s$; ($\lambda$$e$.es{-}knows\{i:l\}(${\it poss}$; $R$; $P$; $e$)); ${\it Rs}$; $R$)
\-
\end{tabbing}